COMMENT ā VALID 00002 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 (get-proofs lispax prf prf jk) C00003 ENDMK Cā; (get-proofs lispax prf prf jk) (tty |you are now at the end of the proof lispax.|)